Boolean satisfiability (SAT) is known in the prior art as an important HP-hard problem with significant commercial CAD and test applications, which include automated timing verification, automated layout, automated routability analysis, logic minimization and automated test pattern generation.